\documentclass[executivepaper,spanish,10pt]{article}
\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}

%\usepackage{a4wide}
\usepackage{caratula}
\usepackage{tad}
\usepackage{algo2symb}

\usepackage[left=1.5cm,top=1.5cm,right=1cm,nohead,nofoot]{geometry}

\begin{document}
    \materia{Algoritmos y Estructuras de Datos II}
    \titulo{Trabajo Practico 1}
    \subtitulo{Mini-Monopoly}
    \grupo{Grupo ...}
    \integrante{Pablo Javier Monzon}	{196/04}{pablo@alone-i-break.com.ar}
    \integrante{Nicolas Orcali}		{139/07}{lordaratur@hotmail.com}
    \integrante{Daniel Jorge Pino}	{556/07}{jdanielpino@gmail.com}
    \integrante{Juan Pablo Sormani}	{604/06}{sorman@gmail.com}
    \maketitle

%\tableofcontents
%\newpage

%\section{Consideraciones}
%
%\begin{itemize}
%\item{ Chamuyo 1 }
%\item{ chamuyo 2 }
%\end{itemize}

\newpage
\section{Juego}
\begin{tad}{ESTANCIERO}
\\
\hrule
\usa{JUGADOR, TABLERO, BOOL EXTENDIDO}
\generos{estanciero}
\exporta{estanciero, generadores, observadores, otras operaciones}

\igualobs{j}{k}{juego}{JugadorActual(j) JugadorActual(k) \land $\\$
 SueldoInicial(j) = SueldoInicial(k) \land $\\$
 JugadoresActivos(j) = JugadoresActivos(k) \land $\\$
 Tablero(j) = Tablero(k) \land $\\$
 (\forall j_2 : jugador) DineroJugador(j_2,j) = DineroJugador(j_2,k) \land $\\$
 EstadiaEnCarcel(j_2,j) \land EstadiaEnCarcel(j_2,k) \land $\\$
 (\forall c : casilla) CasillaComprada(c,j) = CasillaComprada(c,k) \land $\\$
 DuenodeCasilla(c,j) = DuenodeCasilla(c,k) }

\generadores

    \alinearfuncs{NuevoJuego}{secu(jugador)/jugadores, tablero/t, nat/patrimonio}

    \func{NuevoJuego}{secu(jugador)/jugadores, tablero/t, nat/patrimonio}{estanciero}{}
    \func{TirarDado}{estanciero/e, dados/d}{estanciero}{}
    \func{ComprarPropiedad}{restaurant/r, mesa/m, plato/p}{estanciero}
	{PropiedadComprable?(CasillaActual(JugadorActual(e)),JugadorActual(e),e)}

\observadores

    \alinearfuncs{CasillaComprada?}{estanciero/e, casilla/c}
    \func{JugadorActual}{estanciero/e}{estanciero}{}
    \func{SueldoInicial}{estanciero/e}{nat}{}
    \func{DineroJugador}{estanciero/e, jugador/j}{nat}{}
    \func{CasillaComprada?}{estanciero/e, casilla/c}{bool}{}
    \func{EstadiaEnCarcel}{estanciero/e, jugador/j}{nat}{}
    \func{JugadoresActivos}{estanciero/e}{secu(jugador)}{}
    \func{Tablero}{estanciero/e}{tablero}{}
    \func{DuenodeCasilla}{estanciero/e}{jugador}{CasillaComprada?(e,c)}
    \func{CasillaActual}{estanciero/e, jugador/j}{Casilla}{}


\otrasops

    \alinearfuncs{PropiedadComprable?}{estanciero/e, casilla/c, jugador/j}
    \func{TerminoJuego?}{estanciero/e}{bool}{}
    \func{PropiedadComprable?}{estanciero/e, casilla/c, jugador/j}{bool}{}
    \func{PosicionActual}{estanciero/e, jugador/j}{nat}{}
    \func{Quebrado?}{estanciero/e, jugador/j}{Bool}{}
    \func{vueltas}{estanciero/e, dados/d}{Nat}{}

\axiomas{($\forall$ j:jugador, t:tablero, c:casilla, e:estanciero, d:dados)}

  \alinearaxiomas{mesasAsignadas(inaugurar(menu,diccMozos))}
	\axioma{JugadorActual(NuevoJuego(s,t,patri,sueldo) )}{prim(JugadoresActivos(j))}
	\axioma{JugadorActual(TirarDado(j,d) )}{prim(JugadoresActivos(j))}
	\axioma{JugadorActual(ComprarPropiedad (j) )}{prim(JugadoresActivos(j))}

	\axioma{SueldoInicial(NuevoJuego(s,t,patri,sueldo) )}{patri}
	\axioma{SueldoInicial(TirarDado(j,d) )}{SueldoInicial(j)}
	\axioma{SueldoInicial(ComprarPropiedad (j) )}{SueldoInicial(j)}
	
	
	\axioma{DineroJugador(NuevoJuego(s,t,patri,sueldo), j)}{patri}
	\axiomalargo{DineroJugador(tirarDado(e,d), $j_2$)}{\begin{tabbing}
		oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=\kill\+\+\+\\
		if (JugadorActual(j) == $j_2$ ) then \+\\
			DineroJugador(j,$j_2$) + vueltas(e,d) * SueldoInicial(j) \\
			if(CasillaComprada?(CasillaActual(tirarDado(j,d), $j_2$), j) then \+\\
				valor(CasillaActual(tirarDado(j,d), $j_2$) div 10 \-\\
			else \+\\
				0 \-\\
			endif \-\\
		 else \+\\
			if(duenoDeCasilla(CasillaActual(tirarDado(j,d))) == $j_2$) then \+\\
				if quebrado?(JugadorActual(j),j) then \+\\
					DineroJugador(j,$j_2$) + DineroJugador(j,jugadorActual(j)) \-\\
				else \+\\
					DineroJugador(j,$j_2$) + valor(CasillaActual(tirarDado(j,d), $j_2$) div 10\-\\
			else \+\\
				DineroJugador(j,$j_2$) \-\\
			endif \-\\
		endif \\
	\end{tabbing}	
	}
	\axiomalargo{DineroJugador(ComprarPropiedad(j), $j_2$)}{\begin{tabbing}
		oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=oooo\=\kill\+\+\+\\
		if (JugadorActual(j) == $j_2$ ) then \+\\
			DineroJugador(j,$j_2$) - valor(CasillaActual($j_2$,j)) \-\\
		else \+\\
			DineroJugador(j,$j_2$) \-\\
		endif \\
	\end{tabbing}
	}
	\alinearaxiomas{CasillaComprada?(NuevoJuego(s,t,patri,sueldo), c)}
	\axioma{CasillaComprada?(NuevoJuego(s,t,patri,sueldo), c)}{False}
	\axioma{CasillaComprada?(TirarDado(j,d), c)}{CasillaComprada? (j,c)}
	\axioma{CasillaComprada?(ComprarPropiedad (j), $c_2$ )}{
		if (CasillaActual(j) == $c_2$) then \\
			true \\
		else \\
			CasillaComprada? ( j, $c_2$ ) \\
		endif \\
	}
	\alinearaxiomas{EstadiaEnCarcel?(NuevoJuego(s,t,patri,sueldo), $j_2$)}
	\axioma{EstadiaEnCarcel?(NuevoJuego(s,t,patri,sueldo), $j_2$)}{0}
	\axioma{EstadiaEnCarcel?(TirarDado(j,d), $j_2$)}{
		if (EstadiaEnCarcel (j,$j_2$) == 0 $\land$ \\
	        esCarcel?(CasillaActual($j_2$, TirarDado(j,d), $j_2$)) ) then \\
			1 \\
	        else \\
			if EstadiaEnCarcel? (j,$j_2$) $\neq$ 3 then \\
				0 \\
	        	else \\
				if EstadiaEnCarcel? (j,$j_2$) $\ge$ 1 $\land$ $\not$ sonIguales(d) then \\
					EstadiaEnCarcel? (j,$j_2$)+1 \\
	         		else \\
					EstadiaEnCarcel? (j,$j_2$) \\
				endif \\
			endif \\
		endif \\
	}
	\axioma{EstadiaEnCarcel? ( ComprarPropiedad (j), $j_2$)}{EstadiaEnCarcel?(j,$j_2$)}
	
	\axioma{JugadoresActivos ( NuevoJuego(s,t,patri,sueldo) )}{s}
	\axioma{JugadoresActivos ( TirarDado(j,d) )}{
		if (DineroJugador( tirarDado(j,d) , JugadorActual(j)) < 0 ) then \\
			fin(jugadoresActivos(j) \\
		else \\
			fin(jugadoresActvidos(j)°prim(JugadoresActivos(j)) \\
		endif
	}
	\axioma{JugadoresActivos ( ComprarPropiedad (j) )}{JugadoresActivos(j)}
	
	\axioma{Tablero ( NuevoJuego(s,t,patri,sueldo) )}{t}
	\axioma{Tablero ( TirarDado(j,d) )}{Tablero (j)}
	\axioma{Tablero ( ComprarPropiedad (j) )}{tablero (j)}
	
	\axioma{DuenodeCasilla(TirarDado(j,d), c)}{
		if quebrado(JugadorActual(j),TirarDado(j,d) ) $\land$ DuenodeCasilla(j,c) = JugadorActual(j) then \\
			DuenodeCasilla(j, CasillaActual(TirarDado(j,d), JugadorActual(TirarDado(j,d))) \\
		else \\
			DuenodeCasilla(j,c) \\
		endif
	}
	\axioma{DuenodeCasilla ( ComprarPropiedad (j), $c_2$ )}{
		if (CasillaActual(j) == $c_2$) then \\
			JugadorActual(j) \\
		else \\
			DuenodeCasilla(j,$c_2$) \\
		endif
	}
	\axioma{TerminoJuego(j)}{(JugadoresActivos(j) == 1)}
	
	\axioma{CasillaActual ( NuevoJuego(s,t,patri,sueldo), j)}{prim(tablero(j))}
	\axioma{CasillaActual ( TirarDado(j,d), $j_2$)}{enesimoT(tablero(j), PosicionActual(j,$j_2$))}
	\axioma{CasillaActual ( ComprarPropiedad (j), $j_2$)}{enesimo(tablero(j), PosicionActual(j,$j_2$))}
	
	\axioma{PropiedadComprable?(c,j,jugador)}{(DineroJugador(jugador,j) >= Valor(c)}

%% No tiene mucho sentido ya pasoLaSalida si vamos a calcular las veces que paso por la salida
%	\axioma{pasoLaSalida ( NuevoJuego(s,t,patri,sueldo), j)}{False}
%	\axioma{pasoLaSalida ( TirarDado(j,d), $j_2$)}{PosicionActual(j,$j_2$) + Suma(d) > cardinal(Casillas(Tablero(j)))}
%	\axioma{pasoLaSalida ( ComprarPropiedad (j), $j_2$)}{pasoLaSalida(j,$j_2$)}

	\axioma{PosicionActual ( NuevoJuego(s,t,patri,sueldo), j)}{0}
	\axioma{PosicionActual ( TirarDado(j,d), $j_2$)}{
		PosicionActual (j,$j_2$) + Suma(d) mod cant(Casillas(Tablero(j)))
	}
	\axioma{PosicionActual ( ComprarPropiedad (j), $j_2$)}{PosicionActual(j,$j_2$)}
	\axioma{Quebrado? (j,$j_2$)}{
		if (CasillaComprada?(CasillaActual(j,$j_2$),j)) then \\
			DineroJugador(j,$j_2$) < Valor(CasillaActual(j,$j_2$)) \\
		else \\
			false \\
		endif
	}

	\axioma{vueltas(e,d)}{(PosicionActual(e, JugadorActual(e)) + suma(d)) div longitud(casillas(tablero(e)))}

\end{tad}

\input{casilla}

\newpage
\input{dados}

%\newpage
\input{tablero}

\hrule

$ $\\
TAD JUGADOR es STRING \\
%TAD TABLERO es secu(CASILLA)\\

\end{document}
